Inference at * 1 
Iof proof for Lemma decidable implies better:



1. P : 
2. Q : x:P.
3. Dec(P)
  (P  Dec(Q))  Dec(P  Q) 

latex

 by D 0 

latex

 1: 

 1: 4. P  Dec(Q)
 1:   Dec(P  Q)
 2: .....wf..... NILNIL

 2:   (P  Dec(Q))  
 .

Definitions

P  Q, Dec(P)